During verification, verification tools may receive a connectivity specification that captures the source signal, the destination signal, and the condition (e.g., conditions due to multiplexers) and/or latency (e.g., timing delay due to flip-flops) in which the source and destination signals are connected. The specification may be further translated into a property to be proved or disproved by the verification tools. During a verification flow for a data flow network, one piece of data is transmitted within the network and is compared with one or more other pieces of data to determine whether one or properties may be proved or disproved or one or more states may be reachable.
Conventional verification approaches compare the values of variables representing data propagating within a network. For example, these conventional verification approaches use 256 values for comparisons of 8-bit variables or words. With the increasing complexities of modern electronic designs and hence the numerosity and complexity of properties to be verified, a challenge arose in domain reduction where several attempts have been made to reduce the data flow and thus the size of the domain for verification.
Modern electronic designs such as various general purpose processors, embedded systems, special purpose processors not only have more substantially more circuit components and more complex logic but also a longer word size (e.g., 64-bit, 128-bit, etc.) The increasing number of circuit components, more complex logic, and increasing widths of data further exacerbate the performance of verification tools due to the ever increasing domain sizes of modern electronic designs.
Therefore, there exists a need for a method, system, and computer program product for simplifying an electronic design for verification by domain reduction.